perm filename EQUIV.MEM[S79,JMC] blob
sn#453708 filedate 1979-06-25 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 % A SIMPLE SET THEORY PROOF IN FOL
C00020 ENDMK
C⊗;
% A SIMPLE SET THEORY PROOF IN FOL
%
% Stimulated by Don Knuth's remark that proving the existence of the
% set of equivalence classes of an equivalence relation was several hundred
% steps in AUTOMATH, I decided to see what it came to in FOL.
% We prove that the set of equivalence classes exists, that the union
% of the classes is the original set, that the elements of each class
% are mutually equivalent and that if two classes intersect they are
% equal.
%
% The FOL proof of the existence and some properties of the set
% equivalence classes modulo an equivalence relation came to 102
% steps. If it were done over, about 10 steps would be removed with
% some improvement in clarity. We begin with a set of axioms for Zermelo-
% Fraenkel set theory. They have been used in other proofs and only a few
% of them are used in this proof.
%
% The axioms begin with declarations of symbols. Formal declaration
% statements are a feature FOL shares with programming languages. There are
% two axiom schemata - replacement and separation - and both are used in
% the proof.
%
% Then we have the axioms for an equivalence relation R(x,y). Further
% comments are included with the proof itself.
COMMENT ! Axioms for Zermelo-Fraenkel Set Theory AJT June 75, modified JMC !
DECLARE INDCONST nl int;
DECLARE PREDCONST ε 2[INF];
DECLARE PREDCONST ⊂ 2[INF];
DECLARE OPCONST ∪ 2[INF];
DECLARE OPCONST ∩ 2[INF];
DECLARE OPCONST union 1[pre];
DECLARE OPCONST intersect 1[pre];
DECLARE INDVAR r s t u v w x y z;
DECLARE PREDPAR A 2 B 1;
AXIOM ZF:
EXT: ∀x y.(∀z.(zεx≡zεy)≡x=y); % Extensionality
EMT: ∀y.¬yεnl; % Null set
PAIR: ∀x y w.(wε{x,y}≡w=x∨w=y); % Unordered pair
UNION: ∀x z.(zεunion(x)≡∃t.(tεx∧zεt)); % Sum set
INTERSECT: ∀x z.(zεintersect(x)≡∀t.(tεx⊃zεt)); % Product set
INF: (0εint∧∀y.(yεint⊃(y∪{y})εint)); % Infinity
INDUCT: B(0)∧∀x.(xεint∧B(x)⊃B(x∪{x}))⊃∀x.(xεint⊃B(x)); % Induction
REPL: ∀x.∃y.∀z.(A(x,z)≡y=z) ⊃ % Replacement
∀u.∃v.(∀r.(rεv ≡ ∃s.(sεu∧A(s,r))));
SEP: ∀x.∃y.∀z.(zεy≡zεx∧B(z)); % Separation
POWER: ∀x.∃y.∀z.(zεy≡z⊂x); % Power set
REG: ∀x.∃y.(x=0∨(yεx∧∀z.(zεx⊃¬zεy)));;; % Regularity
DECLARE PREDCONST FUN 1,INTO 2,PSUBSET 2[INF];
DECLARE OPCONST rng 1 dom 1;
AXIOM
SUBSET: ∀x y.(x⊂y≡∀z.(zεx⊃zεy));
PROPSUBSET: ∀x y.(PSUBSET(x,y)≡x⊂y∧¬x=y);
PAIRFUN: ∀x y z.(zε{x,y}≡z=x∨z=y);
UNITSETFUN: ∀x.( {x}={x,x} );
OPAIRFUN: ∀x y.( <x,y>={{x},{x,y}} );
FUNCTION: ∀w.(FUN(w)≡∀z.(zεw⊃∃x y.(z=<x,y>))∧
∀x y z.(<x,y>εw∧<x,z>εw⊃y=z) );
DOMAIN: ∀w x.(xεdom(w)≡FUN(w)∧∃y z.(yεw∧y=<x,z>));
RANGE: ∀w x.(xεrng(w)≡FUN(w)∧∃y z.(yεw∧y=<z,x>));
INTO: ∀w x.(INTO(w,x)≡rng(w)⊂x);
SUM: ∀x y z.(zεx∪y≡zεx∨zεy);
PRODUCT: ∀x y z.(zεx∩y≡zεx∧zεy); ;
COMMENT !Axioms about an equivalence relation R(x,y)!
DECLARE PREDPAR R 2;
AXIOM EQUIV: ∀x.R(x,x)
∀x y.(R(x,y) ≡ R(y,x))
∀x y z.(R(x,y) ∧ R(y,z) ⊃ R(x,z));;
DECLARE INDVAR a;
DECLARE INDVAR r1 r2;
% The proof begins with a use of the axiom schema of replacement aimed
% at defining the set of equivalence classes as the image of the set a under
% the mapping that takes each element of a into its equivalence class. The
% schema gives rise to an implication the premiss of which is that the
% relation defines a mapping. In order to prove this, we must establish
% the existence of a unique equivalence class as a set. This is begun by
% the second step which uses the separation schema to define the equivalence
% class of an element. Step 19 is the premiss of step 1. Its proof
% does not use the fact that R(x,y) is an equivalence relation. More comments
% after step 21.
*****∧i REPL[A←λx t.(∀y.(yεt ≡ yεa ∧ R(x,y)))];
1 ∀x.∃y.∀z.(∀y.(yεz≡(yεa∧R(x,y)))≡y=z)⊃∀u.∃v.∀r.(rεv≡∃s.(sεu∧∀y.(yεr≡(yεa∧R(s,y)))))
*****∧i SEP[B←λy.R(x,y)];
2 ∀x1.∃y.∀z.(zεy≡(zεx1∧R(x,z)))
*****∀E ↑ a;
3 ∃y.∀z.(zεy≡(zεa∧R(x,z)))
*****∃E ↑ w;
4 ∀z.(zεw≡(zεa∧R(x,z))) (4)
*****ASSUME ∀z.(zεt≡(zεa∧R(x,z)));
5 ∀z.(zεt≡(zεa∧R(x,z))) (5)
*****∀E EXT w,t;
6 ∀z.(zεw≡zεt)≡w=t
*****∀E ↑↑↑ z;
7 zεw≡(zεa∧R(x,z)) (4)
*****∀E ↑↑↑ z;
8 zεt≡(zεa∧R(x,z)) (5)
*****TAUT zεw≡zεt 7:8;
9 zεw≡zεt (4 5)
*****∀I ↑ z;
10 ∀z.(zεw≡zεt) (4 5)
*****TAUT w=t 6,10;
11 w=t (4 5)
*****⊃I 5⊃↑;
12 ∀z.(zεt≡(zεa∧R(x,z)))⊃w=t (4)
*****ASSUME w=t;
13 w=t (13)
*****SUBST ↑ IN 4;
14 ∀z.(zεt≡(zεa∧R(x,z))) (4 13)
*****⊃I ↑↑⊃↑;
15 w=t⊃∀z.(zεt≡(zεa∧R(x,z))) (4)
*****TAUT ∀z.(zεt≡(zεa∧R(x,z)))≡w=t 12,15;
16 ∀z.(zεt≡(zεa∧R(x,z)))≡w=t (4)
*****∀I ↑ t;
17 ∀t.(∀z.(zεt≡(zεa∧R(x,z)))≡w=t) (4)
*****∃I ↑ w←y;
18 ∃y.∀t.(∀z.(zεt≡(zεa∧R(x,z)))≡y=t)
*****∀I ↑ x;
19 ∀x.∃y.∀t.(∀z.(zεt≡(zεa∧R(x,z)))≡y=t)
*****TAUT ∀u.∃v.∀r.(rεv≡∃s.(sεu∧∀y.(yεr≡(yεa∧R(s,y))))) 1,19;
20 ∀u.∃v.∀r.(rεv≡∃s.(sεu∧∀y.(yεr≡(yεa∧R(s,y)))))
*****∀E ↑ a;
21 ∃v.∀r.(rεv≡∃s.(sεa∧∀y.(yεr≡(yεa∧R(s,y)))))
% We now have the required set of equivalence classes, and the rest of
% proof is concerned with establishing its properties. By step 53 we
% have established that the union of the set v of equivalence classes
% is the set a. It uses only the reflexivity of R(x,y). Step 68
% asserts that all the elements of an equivalence class are equivalent,
% and its proof uses the symmetry and transitivity of R(x,y). Step 99
% asserts that if two equivalence classes intersect they are equal, and
% the remaining three steps package these results into a single statement.
% Neither FOL's sort mechanism nor any of its methods of simplification
% are used in the proof. and it doesn't seem that they would help much.
% It seems possible that Juan Bulnes's goal oriented FOL would allow
% a considerably shorter proof.
*****∃E ↑ v;
22 ∀r.(rεv≡∃s.(sεa∧∀y.(yεr≡(yεa∧R(s,y))))) (22)
*****∀E UNION v;
23 ∀z.(zεunion v≡∃t.(tεv∧zεt))
*****∀E ↑ z;
24 zεunion v≡∃t.(tεv∧zεt)
*****ASSUME zεunion v;
25 zεunion v (25)
*****TAUT ∃t.(tεv∧zεt) 24:25;
26 ∃t.(tεv∧zεt) (25)
*****∃E ↑ t;
27 tεv∧zεt (27)
*****∀E 22 t;
28 tεv≡∃s.(sεa∧∀y.(yεt≡(yεa∧R(s,y)))) (22)
*****TAUT ∃s.(sεa∧∀y.(yεt≡(yεa∧R(s,y)))) 27:28;
29 ∃s.(sεa∧∀y.(yεt≡(yεa∧R(s,y)))) (22 27)
*****∃E ↑ s;
30 sεa∧∀y.(yεt≡(yεa∧R(s,y))) (30)
*****∧E ↑:#2;
31 ∀y.(yεt≡(yεa∧R(s,y))) (30)
*****∀E ↑ z;
32 zεt≡(zεa∧R(s,z)) (30)
*****TAUT zεa 27,32;
33 zεa (22 25)
*****⊃I 25⊃↑;
34 zεunion v⊃zεa (22)
*****ASSUME zεa;
35 zεa (35)
*****∧I SEP[B←λy.R(z,y)];
36 ∀x.∃y.∀z1.(z1εy≡(z1εx∧R(z,z1)))
*****∀E ↑ a;
37 ∃y.∀z1.(z1εy≡(z1εa∧R(z,z1)))
*****∃E ↑ y;
38 ∀z1.(z1εy≡(z1εa∧R(z,z1))) (38)
*****∧I ((35 38));
39 zεa∧∀z1.(z1εy≡(z1εa∧R(z,z1))) (35 38)
*****∃I ↑ z←s;
40 ∃s.(sεa∧∀z1.(z1εy≡(z1εa∧R(s,z1)))) (35 38)
*****∀E 22 y;
41 yεv≡∃s.(sεa∧∀y1.(y1εy≡(y1εa∧R(s,y1)))) (22)
*****TAUT yεv 40:41;
42 yεv (22 35 38)
*****∀E 38 z;
43 zεy≡(zεa∧R(z,z)) (38)
*****∀E EQUIV1 z;
44 R(z,z)
*****TAUT zεy 35,43:44;
45 zεy (35 38)
*****∧I ((42 45));
46 yεv∧zεy (22 35 38)
*****∃I ↑ y←t;
47 ∃t.(tεv∧zεt) (22 35)
*****TAUT zεunion v 24,47;
48 zεunion v (22 35)
*****⊃I 35⊃↑;
49 zεa⊃zεunion v (22)
*****TAUT zεunion v≡zεa 34,49;
50 zεunion v≡zεa (22)
*****∀I ↑ z;
51 ∀z.(zεunion v≡zεa) (22)
*****∀E EXT union v,a;
52 ∀z.(zεunion v≡zεa)≡union v=a
*****TAUT union v=a 51:52;
53 union v=a (22)
*****ASSUME rεv;
54 rεv (54)
*****∀E 22 r;
55 rεv≡∃s.(sεa∧∀y.(yεr≡(yεa∧R(s,y)))) (22)
*****TAUT ∃s.(sεa∧∀y.(yεr≡(yεa∧R(s,y)))) 54:55;
56 ∃s.(sεa∧∀y.(yεr≡(yεa∧R(s,y)))) (22 54)
*****ASSUME xεr∧yεr;
57 xεr∧yεr (57)
*****∃E ↑↑ s;
58 sεa∧∀y.(yεr≡(yεa∧R(s,y))) (58)
*****∧E ↑:#2;
59 ∀y.(yεr≡(yεa∧R(s,y))) (58)
*****∀E ↑ x;
60 xεr≡(xεa∧R(s,x)) (58)
*****∀E ↑↑ y;
61 yεr≡(yεa∧R(s,y)) (58)
*****∀E EQUIV2 s,x;
62 R(s,x)≡R(x,s)
*****∀E EQUIV3 x,s,y;
63 (R(x,s)∧R(s,y))⊃R(x,y)
*****TAUT R(x,y) 57,60:63;
64 R(x,y) (22 54 57)
*****⊃I 57⊃↑;
65 (xεr∧yεr)⊃R(x,y) (22 54)
*****∀I ↑ x y;
66 ∀x y.((xεr∧yεr)⊃R(x,y)) (22 54)
*****⊃I 54⊃↑;
67 rεv⊃∀x y.((xεr∧yεr)⊃R(x,y)) (22)
*****∀I ↑ r;
68 ∀r.(rεv⊃∀x y.((xεr∧yεr)⊃R(x,y))) (22)
*****ASSUME r1εv∧r2εv;
69 r1εv∧r2εv (69)
*****ASSUME ∃x.(xεr1∧xεr2);
70 ∃x.(xεr1∧xεr2) (70)
*****∀E 22 r1;
71 r1εv≡∃s.(sεa∧∀y.(yεr1≡(yεa∧R(s,y)))) (22)
*****∀E 22 r2;
72 r2εv≡∃s.(sεa∧∀y.(yεr2≡(yεa∧R(s,y)))) (22)
*****TAUT ∃s.(sεa∧∀y.(yεr1≡(yεa∧R(s,y)))) 69,71;
73 ∃s.(sεa∧∀y.(yεr1≡(yεa∧R(s,y)))) (22 69)
*****TAUT ∃s.(sεa∧∀y.(yεr2≡(yεa∧R(s,y)))) 69,72;
74 ∃s.(sεa∧∀y.(yεr2≡(yεa∧R(s,y)))) (22 69)
*****∃E ↑↑ s;
75 sεa∧∀y.(yεr1≡(yεa∧R(s,y))) (75)
*****∃E ↑↑ t;
76 tεa∧∀y.(yεr2≡(yεa∧R(t,y))) (76)
*****∧E ↑↑:#2;
77 ∀y.(yεr1≡(yεa∧R(s,y))) (75)
*****∧E ↑↑:#2;
78 ∀y.(yεr2≡(yεa∧R(t,y))) (76)
*****∀E ↑↑ x;
79 xεr1≡(xεa∧R(s,x)) (75)
*****∀E ↑↑ x;
80 xεr2≡(xεa∧R(t,x)) (76)
*****∀E 77 w;
81 wεr1≡(wεa∧R(s,w)) (75)
*****∀E 78 w;
82 wεr2≡(wεa∧R(t,w)) (76)
*****LABEL A;
*****∃E 70 x;
83 xεr1∧xεr2 (83)
*****∀E EQUIV2 s,w;
84 R(s,w)≡R(w,s)
*****∀E EQUIV2 x,t;
85 R(x,t)≡R(t,x)
*****∀E EQUIV2 w,t;
86 R(w,t)≡R(t,w)
*****∀E EQUIV2 x,s;
87 R(x,s)≡R(s,x)
*****∀E EQUIV3 w,s,x;
88 (R(w,s)∧R(s,x))⊃R(w,x)
*****∀E EQUIV3 w,x,t;
89 (R(w,x)∧R(x,t))⊃R(w,t)
*****∀E EQUIV3 w,t,x;
90 (R(w,t)∧R(t,x))⊃R(w,x)
*****LABEL B;
*****∀E EQUIV3 w,x,s;
91 (R(w,x)∧R(x,s))⊃R(w,s)
*****TAUT wεr1≡wεr2 79:B;
92 wεr1≡wεr2 (22 69 70)
*****∀I ↑ w;
93 ∀w.(wεr1≡wεr2) (22 69 70)
*****∀E EXT r1,r2;
94 ∀z.(zεr1≡zεr2)≡r1=r2
*****TAUT r1=r2 93:94;
95 r1=r2 (22 69 70)
*****⊃I 70⊃↑;
96 ∃x.(xεr1∧xεr2)⊃r1=r2 (22 69)
*****⊃I 69⊃↑;
97 (r1εv∧r2εv)⊃(∃x.(xεr1∧xεr2)⊃r1=r2) (22)
*****TAUT ((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2 97;
98 ((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2 (22)
*****∀I ↑ r1 r2;
99 ∀r1 r2.(((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2) (22)
*****TAUT union v=a∧(∀r.(rεv⊃∀x y.((xεr∧yεr)⊃R(x,y)))∧∀r1 r2.(((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2)) 53,68,99;
100 union v=a∧(∀r.(rεv⊃∀x y.((xεr∧yεr)⊃R(x,y)))∧∀r1 r2.(((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2)) (22)
*****∃I ↑ v ;
101 ∃v.(union v=a∧(∀r.(rεv⊃∀x y.((xεr∧yεr)⊃R(x,y)))∧∀r1 r2.(((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2)))
*****∀I ↑ a;
102 ∀a.∃v.(union v=a∧(∀r.(rεv⊃∀x y.((xεr∧yεr)⊃R(x,y)))∧∀r1 r2.(((r1εv∧r2εv)∧∃x.(xεr1∧xεr2))⊃r1=r2)))
% I note that I haven't proved that v is unique. This is easy, but
% it would be an automatic byproduct a version of the replacement schema
% stating the true fact that the image set is unique. Thus uniqueness doesn't
% depend on the properties of R(x,y).